p,q:. g:. (a,b,x,y:. ((p = (a * g))  (q = (b * g))  (((x * a) + (y * b)) = 1))) 

latex

Definitions	A c B, guard(T), sq_type(T), P  Q, P  Q, has-value(a), lelt(i; j; k), , int_seg(i; j), int_nzero, prop{i:l}, P  Q, , x:A. B(x), nequal(T; a; b), False, A, A  B, ge(i; j), P  Q, t  T, x:A. B(x), P  Q, decidable(P)
Lemmas	mul assoc, decidable le, absval zero, not functionality wrt iff, sign-absval, sign-squared, add functionality wrt eq, sign wf, absval wf, mul add distrib, rem bounds 1, div rem sum, nequal wf, divide wfa, le wf, decidable int equal, ge wf, nat properties, int seg wf, nat wf